% !Mode:: "TeX:UTF-8"
\documentclass[14pt, twoside]{extreport}
\usepackage{cmap}

%\usepackage{fix-cm}
\usepackage[utf8]{inputenx}
\usepackage[russian]{babel}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%\usepackage{pscyr}
%\usepackage[T1]{fontenc} %cm-super
%\usepackage{type1cm}
\usepackage{indentfirst}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsmath}
%\usepackage{dsfont}
\usepackage{xspace}
\usepackage[numbers,compress,sort]{natbib}
\usepackage{clrscode}

\pagestyle{headings}

\textheight 23cm % 29.7-2-2
\textwidth 16cm % 21-2.5-1.5
\hoffset 0.46cm %2.5-2.54 слева 3 см
\voffset -0.54cm %2-2.54 сверху 2 см
\oddsidemargin 0cm \evensidemargin 0cm  \headheight 0cm \headsep 1.5cm \topmargin 0cm

\usepackage{ccaption} % заменяем для рисунков ':' после номера рисунка на другой символ
\captiondelim{. } % разделитель точка и пробел

\usepackage[off]{auto-pst-pdf}

\usepackage{ifpdf}

\usepackage{vaucanson-g}

\ifpdf
% we are running pdflatex, so convert .eps files to .pdf
% run pdflatex with --shell-escape and thesis.aux
%\usepackage[pdftex]{graphicx}
\usepackage{epstopdf}
\else
% we are running LaTeX, not pdflatex
\usepackage{graphicx}
\fi

% Подправим команду \appendix : нумерация русскими буквами,
% а не латинскими.
\makeatletter
\renewcommand\appendix{\par
  \setcounter{chapter}{0}%
  \setcounter{section}{0}%
  \def\@chapapp{\appendixname}%
  \def\thechapter{\@Asbuk\c@chapter}}
\makeatother

% "русифицируем" окружение enumerate:
\makeatletter
\def\labelenumi{\theenumi)}      % чтобы после номера шла скобка;
\def\theenumii{\@asbuk\c@enumii}   % чтобы на втором уровне шли русские,
\def\labelenumii{\theenumii)}    % а не латинские буквы
\def\p@enumii{\theenumi}         % а это для \ref
\def\labelenumiii{{\bf--}}       % а на третьем уровне пусть будут лишь тире,
\let\theenumiii\relax            % и отдельных ссылок на него не будет
\def\p@enumiii{\theenumi\theenumii}
\makeatother

\usepackage{rsl}

\usepackage{listingsutf8}
\lstloadlanguages{RSL}
\lstset{numbers=left, language=RSL, extendedchars=true, numberstyle=\tiny, inputencoding=utf8%,
%commentstyle=\itshape, stringstyle=\bfseries
}

\author{Евгений Корныхин}
\title{\huge{\textbf{\textsc{Формальная спецификация программ. Модель с внутренним состоянием}}}}
%\date{Москва --- 2010}

\newcounter{problem_type}[chapter]
\newcounter{zadacha}[problem_type]
\newcommand{\z}{\vspace{0.5cm}\par\addtocounter{zadacha}{1}%
\textit{\arabic{chapter}.\arabic{problem_type}.\arabic{zadacha}}~~  }

%\newcounter{problem_type}[section]
%\newcounter{zadacha}[problem_type]
%\newcommand{\z}{\vspace{0.5cm}\par\addtocounter{zadacha}{1}%
%\textit{\arabic{section}.\arabic{problem_type}.\arabic{zadacha}}~~  }

\newcommand{\head}[1]{\vspace{1cm}\subsubsection*{#1}}
\newcommand{\zhead}[1]{\head{#1} \refstepcounter{problem_type}}


\begin{document}

\maketitle

\tableofcontents \pagebreak

%\chapter*{Введение}
%\addcontentsline{toc}{chapter}{Введение}

\input{intro}


\section*{Модели программ с внутренним состоянием}
\addcontentsline{toc}{chapter}{Модели программ с внутренним состоянием}

В рамках этого курса будут рассматриваться только  программы, для которых можно составить модель с внутренним состоянием.

Можно себе представить такую модель как черный ящик, способный принимать входные воздействия (название \emph{операции} и ее аргументы) и выдавать ответ (см. рисунок~\ref{fig:machine}). Например, операция --- возведение в квадрат, аргумент --- число 2, результат --- число 4. 

\begin{figure}[h] \center
  \includegraphics[width=0.7\textwidth]{rsl/machine}\\
  \caption{Модель программы с внутренним состоянием}\label{fig:machine}
\end{figure}

Например, для модели программы-калькулятора операцией будет выполнение некоторого арифметического действия или ввод числа.

По сравнению с реальной программной системой в рассматриваемой нами модели нет таких понятий, как время выполнения операции и параллельное выполнение операций. Иными словами, <<операция>> аналогична функциям, в математическом смысле (функция --- как отображение входных данных к выходным, а не как подпрограмма). Но хотя нет понятия времени выполнения операции, есть понятие последовательности операций над системой.

Однако в этой модели выдача результата-значения  (как в примере с возведением в квадрат числа 2) не является обязательной и однозначной. А именно,
\begin{enumerate}
	\item на входное воздействие модель может ответить тем, что она перестает выдавать ответы вообще (<<зацикливается>>);
	\item на одни и те же входные воздействия модель может выдать различные ответы (модель недетерминирована);
	\item модель может ничего не ответить на входное воздействие в виде результата, но при этом может оказать \emph{побочный эффект}, и после этого продолжать выдавать ответы на следующие входные воздействия.
\end{enumerate}

Для нас важно, что на такой модели можно <<формулировать свойства>>, т.е. можно дать определение \emph{правильной} системы с теми же названиями операций. Правильная система --- та, что правильно выполняет операции, поддерживает внутреннюю согласованность своих компонентов (согласованность внутреннего состояния), некоторым заданным образом изменяет состояние среды, в которой она работает.

Попытка даже просто сформулировать такие свойства (т.е. проделать дополнительную работу в плюс к проектированию и кодированию программной системы) дает много преимуществ. Во-первых, это позволяет по-иному взглянуть на разрабатываемую систему, увидеть то, что до этого не было явно сказано, и, возможно, такой взгляд позволит увидеть ряд дефектов в проекте или даже исходном тексте (например, если в исходном тексте был упущен какой-нибудь случай в работе системы). Во-вторых, поскольку свойства записаны на формальном языке, возможна автоматическая проверка как самих записанных свойств (на полноту, на согласованность), так и проверка соответствия свойств и других артефактов разработки системы (например, соответствия свойств исходному тексту программы).

Сначала надо попробовать почувствовать этот <<иной взгляд>>, для чего вам будет предложено сделать ряд упражнений (см. ниже). А после этого предлагается ознакомиться с формальным языком спецификации, на котором можно записывать свойства моделей.

\section*{Задачи}

\zhead{Для следующих технических средств, идей и технологий сформулируйте не определение, а область применения и эффект от применения этого (эффект должен выражаться в некотором качественном изменении системы, к которой это средство применяется, или среды, где работает эта система)}

\z \emph{вытесняющая многозадачность} (вид многозадачности, при которой операционная система может временно прервать текущий процесс без какой-либо помощи с его стороны)

\textbf{Решение:}

область применения: пользовательские процессы.

эффект от применения: зависший процесс не завешивает всю ОС.

\z \emph{невытесняющая многозадачность}

\z \emph{пакетная обработка заданий}

\textbf{Решение:}

эффект: для вычислительных задач -- максимизация использования вычислительных ресурсов.

\z \emph{разделение времени при обработке заданий}

\z \emph{страничная организация виртуальной памяти}

\z \emph{инвертированная таблица страниц}

\z \emph{регистровые окна}

\z \emph{элеваторный алгоритм планирования дисковых обменов}

\z \emph{файл, отображаемый в память}

\z \emph{динамическая библиотека}

\z \emph{страничный демон}

\z \emph{монитор Хоара}

\z \emph{буферизация ввода/вывода}

\z \emph{дейтаграммные сокеты}

%\zhead{Аналогичная задача для механизмов языков программирования; опишите, какое новое качество программ появляется или изменяется существующее при добавлении этих механизмов в язык}
%
%\z \emph{виртуальные функции}
%
%\z \emph{функции высших порядков}
%
%\z \emph{адресная арифметика}
%
%\z \emph{}
%

	\zhead{Для следующих программ и программных систем привести несколько примеров моделей с внутренним состоянием; какие возможны реализации этих систем, более мощные, чем конечные автоматы?}
		\z Стек.
		\z Почтовый клиент (например, Mozilla Thunderbird или веб-клиент Gmail).
		\z Электронный будильник.
		\z Компьютерная игра <<крестики-нолики>>.
		\z Подсистема работы с вкладками в веб-браузере.
		\z Веб-сайт микроблога (например, Twitter).
		\z Компиляторы gcc.
		\z Игровой веб-сервер для игры в покер. 

%%%%%%%%%% Общая структура %%%%%%%%%%%
%%  0. "Введение". (см. igoogle) Создание формальной модели поведения системы как способ уточнения требований
%%  1. "Основные определения" (спецификация, модель, полнота, тотальность, непротиворечивость, явность).
%%      Нулевая задачка экзамена. Детерминированные функции, недетерминированные функции на примерах чисел.
%%      Первая задачка экзамена в том случае, когда всё состояние скрыто (т.е. про состояние пока что не думаем).
%%  2. "Языки спецификации". Сначала RSL (множества, списки, отображения). Потом ACSL (модель памяти, функции с указателями)
%%  3. "Модельные спецификации". Кроме самих данных, специфицируем состояние системы (модель состояния, инварианты).
%%      Первая задачка экзамена в полном объеме. Выделение ветвей функциональности при записи постусловий.
%%      Согласованность модельных спецификаций (инвариант не пуст после каждой функции, нет вызовов функций вне их предусловий)
%%  4. "Алгебраические спецификации". Понятие алгебраической спецификации (новая вторая задачка экзамена).
%%      Согласованность алгебраических спецификаций (бывшая вторая задачка экзамена).
%%  5. "Автоматные спецификации". Тут про третью задачку экзамена.
%%  6. ......... может быть сюда включить формальную верификацию...........

\chapter{RAISE Specification Language (RSL)}

\section{Сигнатура модели с внутренним состоянием}

%сказать про то, как задавать "интерфейс" модели (как задавать список операций, как задавать состояние, про раздел value и раздел аксиом, в котором будут свойства). Целые числа, примеры моделей с целыми числами и примеры свойств в таких моделях.

Для фиксации рассматриваемых в курсе моделей программ будем пользоваться языком спецификации RSL (Rigorous Approach to Industrial Software Engineering Specification Language). Сейчас рассмотрим синтаксис описания моделей в этом языке. Это описание должно содержать как минимум список операций и список типов аргументов и типов результатов, для каждой операции должна быть указана сигнатура (имя операции, список типов аргументов, список типов результатов операции).

Описание модели без указания операций и типов:

\begin{lstlisting}
scheme MODEL_NAME = class

end
\end{lstlisting}

Описание операций и типов помещается между словами \textbf{class} и \textbf{end}. Описание типа очень простое:

\begin{lstlisting}
scheme STACK = class

type Stack
type Element

end
\end{lstlisting}

Можно объединить объявления типов Stack и Element так:

\begin{lstlisting}
scheme STACK = class

type Stack, Element

end
\end{lstlisting}

За каждым из таких типов закреплено некоторое множество значений и операторы сравнения на равенство/неравенство.

Операции описываются с указанием их имени, типов аргументов и типов результатов. Если типов несколько, они пишутся через символ $\times$. Порядок типов важен. Так описываются операции \emph{в аппликативном стиле}:

\begin{lstlisting}
scheme STACK = class
type Stack, Element

value push : Stack >< Element -~-> Stack

value pop : Stack -~-> Stack >< Element

end
\end{lstlisting}

Внимательный читатель спросит, зачем нужно 2 аргумента для того, чтобы поместить данные в стек? Или, если я хочу достать элемент с вершины стека, зачем я должен передавать еще какой-то аргумент? Дело как раз в аппликативном стиле. В нем мы обязаны передавать полностью всю информацию, которой будет пользоваться операция и какой информацией операция будет отвечать. Полностью --- значит, настоящие аргументы (например, те данные, которые надо положить в стек), состояние окружения модели (если это важно для ее функционирования) и внутреннее состояние модели! В данном случае окружение влияния не оказывает, а внутреннее состояние имеется и его мы указали в качестве дополнительных аргументов (Stack в аргументах и результатах операций).

Как отмечалось ранее, модель может <<зацикливаться>> ~\footnote{на деле модель не зацикливается, это слово выбрано для сокращения ситуации, когда модель перестает отвечать на входные воздействия}, может отвечать недетерминированно. Будем называть операцию модели  \emph{тотальной}, если по этой операции модель не <<зацикливается>> и ведет себя детерминированным образом. Для того, чтобы указать в модели, что некая операция является тотальной, нужно поставить в ее сигнатуре стрелку $\rightarrow$. В прошлом примере тотальной операцией должна быть операция push, а про операцию pop нельзя сказать, что она должна быть тотальной:
\begin{lstlisting}
scheme STACK = class
type Stack, Element

value
	push : Stack >< Element -> Stack,
	pop : Stack -~-> Stack >< Element
end
\end{lstlisting}

Заметим, что указать в операции, что она не должна быть тотальной, нельзя (операция либо только тотальная как push, либо всякая как pop). В последнем примере показано, как задать несколько операций в одной секции \textbf{value}.

Операции push и pop получают аргумент типа Element <<от пользователя>>, а аргумент типа Stack является одним из результатов других push и pop. Но рано или поздно должен найтись, грубо говоря, <<самое старое>>, <<первоначальное>>, значение в типе Stack для операций push или pop (это значение не представимо в виде результата push или pop, для его представления нужно иное средство). Для стека таким <<первоначальным>> значением является пустой стек. Добавим его в модель, такое значение является константой:

\begin{lstlisting}
scheme STACK = class
type Stack, Element

value
	empty : Stack,
	push : Stack >< Element -> Stack,
	pop : Stack -~-> Stack >< Element
end
\end{lstlisting}

\section*{Задачи}

описать сигнатуры операций над моделями, рассмотренными в предыдущих задачах. Указать требование тотальности операций, если операция должна быть тотальной.

\section{Предопределенные типы}

\textbf{Int}, \textbf{Nat}, \textbf{Real}, \textbf{Bool}, \textbf{Char}, \textbf{Text}, \textbf{Unit}.

Тип \textbf{Int} содержит в себе все возможные целые числа. Ограничений на их значения (типа MAXINT) нет.

Тип \textbf{Nat} содержит число 0 и все возможные положительные целые числа. Ограничений сверху на их значения нет. Тип поддерживает все операции, определенные для типа \textbf{Int}. Неограниченные целые числа необходимы для того, чтобы представлять такие заранее неограниченные величины как количества элементов, время (как количество единиц времени).

Тип \textbf{Real} содержит в себе все возможные вещественные числа. Важно понимать, что эти числа являются математической абстракцией тех вещественных чисел, которые представимы в архитектуре компьютера. Тип \textbf{Real} --- это те числа, с которыми работают математики. Следовательно, они включают и все вещественные числа, представимые в какой-угодно архитектуре компьютера. Например, в этом типе есть число <<квадратный корень из двух>>.

Тип \textbf{Bool} содержит булевские значения \textbf{true} и \textbf{false}.

Тип \textbf{Char} содержит все возможные отдельные символы. Этот тип не привязан ни к одной из кодировок (поскольку этот тип --- лишь математическая абстракция). Этот тип содержит все мыслимые символы. Поэтому не определена операция получения <<кода символа>>, привычная для многих языков программирования.

Тип \textbf{Text} является массивом символов (о массивах см.ниже).

Тип \textbf{Unit} является специальным и используется для ограниченного количества случаев (см.ниже). Основное применение --- то же, какое имеет ключевое слово \texttt{void} в сигнатурах функций языка Си.

\head{Операции над встроенными типами}
Арифметические:
\begin{lstlisting}
value
  +: Int >< Int -> Int,
  -: Int >< Int -> Int,
  *: Int >< Int -> Int,
  /: Int >< Int -~-> Int,
  \: Int >< Int -~-> Int,
  **: Int >< Int -~-> Int,
  abs: Int -> Nat,
  real: Int -> Real,

  +: Real >< Real -> Real,
  -: Real >< Real -> Real,
  *: Real >< Real -> Real,
  /: Real >< Real -~-> Real,
  **: Real >< Real -~-> Real,
  abs: Real -> Real,
  int: Real -> Int,

  <: Int >< Int -> Bool,
  <=: Int >< Int -> Bool,
  >: Int >< Int -> Bool,
  >=: Int >< Int -> Bool,

  <: Real >< Real -> Bool,
  <=: Real >< Real -> Bool,
  >: Real >< Real -> Bool,
  >=: Real >< Real -> Bool,

  ~: Bool       -> Bool,
  /\: Bool >< Bool -> Bool,
  \/: Bool >< Bool -> Bool,
  =>: Bool >< Bool -> Bool,
\end{lstlisting}

Для любого типа определены операции сравнения на равенство:
\begin{lstlisting}
type T
value
  = : T >< T -> Bool,
  ~= : T >< T -> Bool
\end{lstlisting}

Порядок вычисления операций строго определен: сначала первый аргумент, затем, если необходимо, второй и т.д.

Логика короткая. Это означает, например, что если первый аргумент конъюнкции равен \textbf{false}, то второй аргумент не вычисляется и вся конъюнкция принимает значение \textbf{false}.

\section*{Задачи}

%TODO
то, что было в задачнике Кузьменковой (запись выражений над предопределенными типами)

\section{Аппликативное описание операций}

RSL не является языком программирования. Однако он позволяет в некоторых несложных случаях написать определение операций в аппликативном (функциональном) стиле. Кроме этого, операции можно реализовать в императивном стиле (этому посвящен раздел~\ref{imperative}).

Рассмотрим простую модель стека: Stack = Nat (количество элементов в стеке). Тогда операции можно определить так:
\begin{lstlisting}
scheme STACK = class
type Stack = Nat, Element

value
   empty : Stack = 0,
	
   push : Stack >< Element -> Stack
   push(s, e) is s+1,
	
   pop : Stack -~-> Stack
   pop(s) is s-1
end
\end{lstlisting}

Можно использовать рекурсию (и, при желании, лямбда-абстракцию):
\begin{lstlisting}
value
   gcd : Nat >< Nat -~-> Nat
   gcd(a, b) is
     if a > b then gcd(b, a)
     elsif a = 0 then b
     else gcd(a, b-a) end
\end{lstlisting}

Так можно записать определение функции, возвращающей несколько значений:
\begin{lstlisting}
value
   minmax : Nat >< Nat -> Nat >< Nat
   minmax(a, b) is
     if a > b then (b, a) else (a, b) end
\end{lstlisting}


\section{Императивное описание операций}\label{imperative}

Теперь посмотрим, как записать определение операции в императивном стиле. Так можно записать \emph{псевдокод алгоритма} Евклида:

\begin{lstlisting}
scheme GCD = class

variable a: Nat, b : Nat

value
  euclid: Unit -~-> write a, b Nat
  euclid() is
     while a > 0 /\ b > 0 do
        if a > b then a := a - b
        else b := b - a end
     end;
     if a = 0 then b else a end
end
\end{lstlisting}

Как видно, язык RSL предлагает использовать такие известные понятия как глобальные переменные, присваивание, последовательности операторов, условный оператор \textbf{if-then-elsif-else-end}, операторы циклов (\textbf{while}), но это ещё не всё. Заметьте, если операции нужно получить доступ к переменной, то это надо указать в сигнатуре операции при помощи ключевого слова \textbf{write} (и \textbf{read}, см. ниже).

\head{Глобальные переменные}
Переменные, определенные вне функции, являются глобальными.
Каждая глобальная переменная должна быть определена в разделе \textbf{variable}, а в сигнатуре функции должен быть указан режим работы функции с переменной: <<только по чтению>> или <<по записи-чтению>>. Функции разрешено оперировать лишь с теми глобальными переменными, которые указаны в сигнатуре. Обращаться к глобальным переменным (даже просто по чтению), не упомянутым в сигнатуре, запрещается. Например,
\begin{lstlisting}
scheme S1 = class
variable status : Text
value
  init : Unit -~-> write status Unit
  init() is (status := "initialized")	
end
\end{lstlisting}

Функция \texttt{init} не имеет аргументов --- для указания этого факта перед стрелкой в сигнатуре функции указан тип \textbf{Unit}. Также у функции нет и результатов. Однако функции разрешено иметь побочный эффект в виде изменения значения глобальной переменной \texttt{status}.

Еще пример:
\begin{lstlisting}[escapechar={|}]
scheme S2 = class
variable status : Text
value
  |is\_initialized| : Unit -~-> read status Bool
  |is\_initialized|() is
	(status = "initialized")	
end
\end{lstlisting}

Здесь глобальная переменная лишь читается в функции, поэтому в сигнатуре переменная \texttt{status} указана с модификатором \textbf{read}.

Можно указать в сигнатуре, что функция может читать или изменять \textbf{любую} глобальную переменную. В этом случае надо после слов \textbf{write} или \textbf{read} вместо имени переменной написать ключевое слово \textbf{any}:
\begin{lstlisting}
scheme S3 = class
   variable a, b : Nat
   value
     sum : Unit -> read any Nat
     sum() is a + b
end
\end{lstlisting}

\head{Тело функции}
Язык RSL позволяет задавать выполнение функции в виде последовательности операторов (операторы разделяются точкой с запятой), условного оператора, операторов цикла, оператора выбора case:
\begin{lstlisting}
scheme S3 = class
	variable a, b : Nat
	value
		swap : Unit -> write a, b Unit
		swap() is
		(
			a := a + b ;
			b := a - b ;
			a := a - b ;
		)
end
\end{lstlisting}

Если функции нужно вернуть некоторое значение, последовательность операторов должна завершаться выражением, чей результат будет результатом работы функции:
\begin{lstlisting}
scheme S4 = class
	variable a, b : Nat
	value
		swap : Unit -> write a, b Nat
		swap() is
		(
			a := a + b ;
			b := a - b ;
			a := a - b ;
			a + b
		)
end
\end{lstlisting}

Среди операторов, объединяемых в последовательность операторов, может быть присваивание, вызов функций, чей возвращаемый тип \textbf{Unit}, условный оператор, оператор цикла.

Условный оператор:
\begin{lstlisting}
scheme S4 = class
	variable a, b : Nat, s : Text
	value
		max : Unit -> read a, b, write s Nat
		max() is
		(
			if a > b then
				s := "first";
				a
			else
				s := "second";
				b
			end
		)
end
\end{lstlisting}

Условный оператор с веткой \emph{elsif}:
\begin{lstlisting}
scheme S4 = class
	variable x : Int, s : Text
	value
		Abs : Unit -> read x, write s Nat
		Abs() is
		(
			if x > 0 then
				s := "positive";
				x
			elsif x = 0 then
				s := "zero";
				0
			else
				s := "negative";
				-x
			end
		)
end
\end{lstlisting}


Операторы циклов (while, do-until и for):

\begin{lstlisting}
variable a: Nat, b : Nat
value
  euclid: Unit -~-> write a, b Nat
  euclid() is
     while a > 0 /\ b > 0 do
        if a > b then a := a - b
        else b := b - a end
     end;
     if a = 0 then b else a end
\end{lstlisting}

\begin{lstlisting}
variable n: Nat, x : Nat
value
  digits: Unit -~-> write n, x Nat
  digits() is
     n := 0;
     do n := n + 1; x := x / 10
     while x = 0;
     n
\end{lstlisting}

\begin{lstlisting}
variable sum : Nat
value
  sumN: Nat -~-> write sum Unit
  sumN(n) is
	sum := 0;
        for i in <.1 .. n.> do
	  sum := sum + i
	end;
\end{lstlisting}

\begin{lstlisting}
variable sum : Nat
value
  sumN: Nat -~-> write sum Unit
  sumN(n) is
	sum := 0; i := 0;
    do
      i := i + 1;
      sum := sum + i
    until i = n	end;
\end{lstlisting}

Способов прервать цикл типа break в RSL нет.

Локальные переменные:
\begin{lstlisting}
variable a: Nat, b : Nat
value
  euclid: Unit -~-> read a, b Nat
  euclid() is
   local variable a1: Nat := a,
                  b1: Nat := b in
     while a1 > 0 /\ b1 > 0 do
        if a1 > b1 then a1 := a1 - b1
        else b1 := b1 - a1 end
     end;
     if a1 = 0 then b1 else a1 end
   end
\end{lstlisting}

%%TODO есть ли неявный LET в императивном стиле ?

\head{Массивы-значения}
В отличие от массивов в императивных языках программирования, понимаемых как непрерывная область памяти однотипных элементов, в RSL массивы ближе к спискам в функциональных языках программирования. Массивы в RSL --- это значения, у которых нет возможности изменить отдельный элемент (можно только заменить всё значение массива целиком). Далее эта особенность будет пояснена на примерах.

Следующая функция использует массив целых чисел:
\begin{lstlisting}
value sort: Int-list -~-> Int-list
\end{lstlisting}

Обращение по индексу делается так: A(1). Нумерация индексов \textbf{с единицы}. Операция \textbf{len} возвращает текущую длину массива. Массивы в RSL могут изменять длину (путем операции конкатенации). Индекс не должен иметь большее значение, чем длина массива, и меньшее, чем 1. Синтаксис RSL запрещает изменять значения отдельных элементов массивов (например, так: <<A(i) := i>>), можно только строить новые массивы целиком (например, вместо <<A(i) := e>> можно писать <<A := $\langle$ if k=i then e else A(k) end | k in $\langle$1 .. \textbf{len} A$\rangle$ $\rangle$>>).

\begin{lstlisting}
value
  sum: Int-list -~-> Int
  sum(ls) is
    local variable s : Int := 0 in
       for i in <.1 .. len ls.> do
             s := s + ls(i)
       end;
       s
    end;
\end{lstlisting}


Эту же функцию, суммирующую элементы массива, можно записать и без использования индексов:
\begin{lstlisting}
value
  sum: Int-list -~-> Int
  sum(ls) is
    local variable s : Int := 0 in
       for l in ls do
             s := s + l
       end;
       s
    end;
\end{lstlisting}

Тип \textbf{Text} является массивом из \textbf{Char}.

Операция \textbf{tl} возвращает <<подмассив>> --- от второго элемента до последнего элемента исходного массива. Операция определена только для непустых массивов. Пустой массив обозначается символом <..>. Тем самым функцию sum можно записать следующим образом с использованием рекурсии:
\begin{lstlisting}
value
  sum: Int-list -~-> Int
  sum(ls) is
    if ls = <..> then 0
    else ls(1) + sum(tl ls) end
\end{lstlisting}


\head{Структуры}
\begin{lstlisting}
type FIO ::
         name : Text
         surname : Text
value
   hello: FIO -~-> Text
   hello(fio) is
      "Hello, " ^ name(fio) ^
           "  " ^ surname(fio) ^ "!"
\end{lstlisting}

Обращение к полю делается в виде вызова функции с именем поля.

\begin{lstlisting}
type FIO ::
         name : Text
         surname : Text
value
   new_fio: Text >< Text -~-> FIO
   new_fio(n,sn) is mk_FIO(n,sn)
\end{lstlisting}

Создание структуры делается с помощью функции с предопределенным именем. Это имя начинается с <<mk\_>>, за которым идет имя типа структуры. В скобках подряд перечисляются выражения, дающие значения полям новой структуры.

\head{Перечисления (enumeration)}
\begin{lstlisting}
type Color = red | blue | white | green
value
  from_rus : Color -~-> Bool
  from_rus(c) is c = red \/ c = blue \/ c = white
\end{lstlisting}

\head{Указатели}
RSL не содержит встроенных механизмов для задания алгоритмов, работающих с указателями и работающих с динамической памятью.

    \section*{Задачи}

    \input{prog/problems}

\section{Множества, списки, отображения}

Более мощные алгоритмы требуют более сложных структур данных. RSL содержит (в дополнение к уже рассмотренным массивам, структурам и перечислениям) средства для работы с множествами, списками и отображениями. 

\input{model/setlist}  % with problems


\section{Эксплицитное и имплицитное описание функций}

Рассмотренный ранее способ описания операций (в виде псевдокода) был \emph{эксплицитным} (explicit, явным) способом описания, поскольку в нем было указано явно <<алгоритм>> вычисления или было дано явное определение функции. Однако, это не единственный способ описания функций в языке RSL.

\emph{Эксплицитным} назовем следующий способ описания функций:
\begin{lstlisting}
value
	funcname : T1 >< ... >< T2 -~-> T3 >< ... >< T4
	funcname(t1, ..., t2) is
		... 
\end{lstlisting}

Т.е. в эксплицитном способе после сигнатуры идет имя функции с формальными аргументами, далее символ $\Is$ и затем выражение, чье значение и есть значение функции.
%Кроме стрелки $\NonDetermFn$ Стрелка в сигнатуре функции может быть любой.

\emph{Имплицитным} назовем следующий способ описания функции:
\begin{lstlisting}
value
	funcname : T1 >< ... >< T2 -~-> T3 >< ... >< T4
	funcname(t1, ..., t2) as (t3, ..., t4)
	post
		... 
\end{lstlisting}

В имплицитном способе после сигнатуры идет имя функции с формальными аргументами, далее слово \textbf{as}, далее формальные имена результатов, далее слово \textbf{post}, после которого идет \textbf{логическое} выражение над именами t1, ..., t2, t3, ..., t4. Т.е. в имплицитном способе описания задается предикат (набор функциональных свойств результата функции), а не <<алгоритм вычисления>>. 

Например:
\begin{lstlisting}
value
	max : Nat >< Nat -> Nat
	max(a, b) as m
	post
		m = a /\ a > b
		\/ m = b /\ a <= b
\end{lstlisting}

Выражение после слова \textbf{post} будем называть \emph{поствыражением}. Функцию из последнего примера можно задать и другим поствыражением:
\begin{lstlisting}
value
	max : Nat >< Nat -> Nat
	max(a, b) as m
	post
		if a > b then m = a 
				else m = b
		end
\end{lstlisting}

Сравните эту запись с эксплицитной записью той же функции:
\begin{lstlisting}
value
	max : Nat >< Nat -> Nat
	max(a, b) is
		if a > b then a 
				else b
		end
\end{lstlisting}


Рассмотрим такое имплицитное определение:
\begin{lstlisting}
value
	max : Nat >< Nat -> Nat
	max(a, b) as m
	post
		a > b => m = a
\end{lstlisting}

Оно отличается тем, что задает функцию max не полностью: если a > b, то известно требование на результат функции (он должен быть равен а), в противном случае поствыражение истинно, а про результат функции ничего не сказано.

Рассмотрим другой пример:
\begin{lstlisting}
value
	max : Nat >< Nat -> Nat
	max(a, b) as m
	post
		m = a \/ m = b
\end{lstlisting}

Здесь точно результат функции не известен ни в одном случае (если числа a и b имеют различные значения). И тем не менее это тоже допустимое и полезное поствыражение.

Иными словами, необходимо понимать следующие возможности:
\begin{itemize}
\item поствыражение должно восприниматься как  \emph{необходимый эффект} функции (если поствыражение, вычисленное на аргументах и результате функции, ложно, значит функция сработала неверно; если поствыражение истинно, ничего нельзя сказать про правильность работы функции); такие поствыражения описывают ту часть функциональности, которая должна быть соблюдена обязательно и неукоснительно, любой <<шаг влево-вправо>> рассматривается самым критичным образом;
\item поствыражение должно восприниматься как  \emph{достаточный эффект} функции (если поствыражение, вычисленное на аргументах и результате функции, истинно, значит функция сработала правильно; в противном случае ничего нельзя сказать о правильности работы функции); такие поствыражения описывают ряд случаев, но, возможно, не весь;
\item поствыражение должно восприниматься как  \emph{необходимый и достаточный эффект} функции.
\end{itemize}

Язык RSL не предоставляет средств для указания того, как должно восприниматься каждое поствыражение. В каждом случае эту <<модальность>> надо оговаривать явно. В дальнейших примерах, если это не сказано явно, будет предполагаться, что поствыражение должно описывать необходимый и достаточный эффект.

Например, ответьте, почему поствыражение в следующем примере задает функцию, не являющуюся максимумом двух чисел, даже несмотря на то, что логика короткая (многие студенты на экзамене ошибочно предполагают, что это поствыражение действительно описывает максимум и применяют подобное <<преобразование>> условного выражения в дизъюнкцию, не замечая совершаемой при этом ошибки):
\begin{lstlisting}
value
	max : Nat >< Nat -> Nat
	max(a, b) as m
	post
		m = a /\ a > b
		\/ m = b
\end{lstlisting}

В поствыражении могут встречаться <<вызовы>> других функций:
\begin{lstlisting}
value
	sum: Nat-list -> Nat
	sum(x) as s
	post
		if x = <..> then s = 0
		else s = sum(tl x) + hd x end
\end{lstlisting}

Вы уже заметили, насколько похожи эксплицитная и имплицитная запись функций. На самом деле если функция не использует глобальных переменных по чтению-записи и завершается с детерминированным результатом, то эксплицитная запись может быть переписана в имплицитном виде очень просто: вместо возвращаемых значений запись равенство, как это было сделано в последних примерах:
\begin{lstlisting}
value max: Nat >< Nat -> Nat
   max(a, b) as m
   post m = (if a > b then a else b end)
\end{lstlisting}

Однако если функция использует глобальные переменные по чтению-записи, то поствыражение должно содержать описание побочного эффекта. Дело в том, что поствыражение нужно для описания результата функции, поэтому:
\begin{enumerate}
\item поствыражение не должно иметь побочного эффекта (а функция может иметь побочный эффект);
\item поствыражение пишется только для функций, которые завершаются и завершаются детерминированным образом (для недетерминированных функций поствыражение ложно).
\end{enumerate}

Итак, если исходная функция имеет побочный эффект, например
\begin{lstlisting}
variable
	a, b : Int
value
	swap : Unit -> write a, b  Unit
	swap() is
		local variable temp : Int := a in
			a := b;
			b := temp
		end
\end{lstlisting} 
то \textbf{эквивалентное}\footnote{слово <<эквивалентное>> ещё раз подчёркивает, что это поствыражение следует воспринимать как необходимое и достаточное описание эффекта функции} определение функции в имплицитном виде полностью сохраняет сигнатуру, а в поствыражение должно входить соотношение значений переменных до вызова функции и значений после вызова функции:
\begin{lstlisting}
variable
	a, b : Int
value
	swap : Unit -> write a, b  Unit
	swap()
	post
		a = b' /\ b = a'
\end{lstlisting}

Штрихованные переменные --- это значения переменных \textbf{до} вызова функции.


%старое \section{Функции в языках спецификации}
%старое  \input{basis/funcs}

    \section*{Задачи}

    \input{alg/formal}

    \input{basis/im2ex}

\zhead{Для следующих эксплицитных заданий функции запишите эквивалентное имплицитное задание без использования рекурсии и циклов}

%TODO задачи с максимумами и поисками элементов !!! из экзамена


\chapter{Контрактные спецификации}

% тут впервые появляется такая вещь, как СВОЙСТВО функций (до этого про свойства не говорили).

% в этой главе появляется понятие о полноте описания
% (полное для одной цели описание может быть неполным для другой!)
% и о недоспецификации (т.е. превыражения!)

%%% на мой взгляд разговор о недетерминированных функциях без упоминания о параллельности и каналах имеет мало смысла !!!

Итак, перед нами либо уже существующая программная система, для которой надо понять, правильная ли она, либо только еще проектируемая. В любом случае мы хотим оценить качество программной системы обоснованным образом, для чего применяем формальные техники. Мы выбрали некоторый уровень абстракции для нашей программной системы, выбрали формализм для составления модели. Теперь мы определяемся с синтаксисом модели (набором идентификаторов: имен констант, имен типов, имен функций --- и их типов и сигнатур). Т.е. сейчас есть некая <<картинка>> (см. рис......), известно, на каких принципах она работает (в данном случае, работает <<как черный ящик>>, принимая на вход операцию с аргументами, тут же выдавая на выход результат и ожидая следующей операции), но не заданы сами операции.

Поэтому теперь <<на этом скелете>> можно формулировать ожидаемые \emph{функциональные свойства} операций: в каких ситуациях каким образом <<ведут себя>> операции (т.е. какой возвращают результат, какой осуществляют побочный эффект). Сейчас мы ограничимся только \emph{свойствами корректности} операций, т.е. это такие свойства, при выполнении которых программную систему можно назвать правильной, а при невыполнении --- нельзя. Поскольку нами выбран формализм, то и свойства корректности мы будет формулировать в рамках этого формализма. А именно, у нас есть входные данные с операциями, выходные данные с операциями, есть внутреннее состояние, есть представление о том, что возможны \emph{цепочки операций}. Значит, у нас есть следующие возможности для выражения того, является ли система правильной:
\begin{itemize}
\item если на допустимые входные данные она возвращает правильно соответствующие им выходные данные;
\item если система никаким воздействием не приводится к недопустимому, несогласованному, разрушающему, внутреннему состоянию (safety).
\end{itemize}
%%TODO а на цепочках, потенциально, можно определить и liveness !!! есть в этом смысл?

Для выражения свойств первого вида применяются \emph{программные контракты}, для выражений свойств второго вида --- \emph{инварианты состояния}.

В заключении хочется ещё раз подчеркнуть, что рассматриваемые в данном курсе формализмы достаточно простые и далеко не единственные в software engineering. Если эти формализмы читателю покажутся недостаточно полезными, имеет смысл посмотреть в сторону других формализмов, но ни в кое случае не <<ставить крест>> сразу на всех формальных методах.

%Виды корректности:
%1) глобальные условия корректности (корректность с точки зрения окружения/пользователя)
%2) корректность взаимодействия компонентов системы
%3) внутренняя корректность компонентов самих по себе
%4) правильный эффект при выполнении операций над системой по отдельности

\section{Программные контракты}\footnote{Текст раздела взят из статьи В.В.Кулямина <<Критерии тестового покрытия, основанные на структуре контрактных спецификаций>>, опубликованная в томе 14 <<Трудов Института системного программирования>>}

Программный контракт операции состоит из предусловия и постусловия. Первое фиксирует требования к корректному использованию этой операции со стороны окружения системы — при каких ограничениях на аргументы обращение к этой операции корректно. Второе определяет обязательства системы по отношению к результатам вызовов этой операции — какие ограничения на результаты работы операции должны быть выполнены при корректной работе системы, если обращение к ней было правильным. При нарушении предусловия операции обращение к ней может иметь любые последствия, поведение системы в этом случае не определено. Совместно пред- и постусловия строго определяют требования к работе системы.

При анализе сложной системы с большим количеством интерфейсных операций крайне неудобно рассматривать их все вместе как однородный набор, необходимо разбиение этих операций на какие-то логические группы по реализуемым ими функциям. Эти группы почти всегда соответствуют компонентам или модулям системы, ответственным за реализацию этих функций. Часто такие компоненты имеют внутреннее состояние, недоступное для непосредственного наблюдения извне системы, но влияющее на поведение вызываемых операций компонента и изменяемое ими.

Поэтому для описания ограничений в пред- и постусловиях необходимо как-то учитывать внутреннее состояние компонента, операции которого описываются. Чтобы сделать это возможным, контракты операций одного компонента объединяются в спецификацию этого компонента вместе с описанием структуры его модельного состояния. Структура модельного состояния компонента не обязана совпадать со структурой его реального состояния, зафиксированной в его коде, например, компонент, реализующий список, может использовать ссылочную структуру данных, в том время, как структура его модельного состояния в спецификациях может быть основана на массиве. В структуре модельного состояния могут совсем отсутствовать некоторые части реального состояния компонента, слабо связанные с его функциональностью, например, различного рода кэши и другие данные, используемые для увеличения производительности. Важно, что структура модельного состояния компонента должна содержать данные, достаточные для полного описания функциональности в пред- и постусловиях операций этого компонента. При этом предусловие зависит от аргументов вызова операции и данных модельного состояния при этом вызове, или пре-состояния. Постусловие зависит как от аргументов и пре-состояния, так и от результата и данных модельного состояния после вызова, или пост-состояния. 

Наличие сложной структуры модельного состояния приводит к необходимости учитывать в контрактах операций ограничения на его данные, которые должны выполняться в стабильных состояниях системы, когда ни одна из операций не выполняется. Такие ограничения оформляются в виде инвариантов модельного состояния. Инварианты являются общими частями пред- и постусловий всех операций, как-то затрагивающих соответствующие компоненты --- они должны выполняться как в пре-состоянии любого вызова, так и в его пост-состоянии.

\section{Ситуации и ветви функциональности}

Обычно постусловие операции описывает несколько разных режимов ее функционирования. Предусловие запрещает все комбинации значений параметров, при которых поведение операции не определено. Однако среди разрешаемых предусловием ситуаций могут остаться такие, в которых выполнить свою основную функцию операция не может. Вместо этого она должна вернуть некоторый код ошибки, создать исключительную ситуацию или как-то иначе сигнализировать о том, что ее основная задача не может быть решена в такой ситуации. Помимо режимов сигнализации о невозможности выполнить основную функцию, само ее выполнение может идти разными путями. Например, операция конкатенации двух строк может проверять, не является ли один из ее аргументов пустой строкой, и в этом случае просто возвращать копию другого аргумента, не выполняя никаких действий над ней. Если же оба аргумента не пусты, копия одного из них должна быть подвергнута модификации, чтобы получить результат операции.

При написании постусловий удобно выделять такие разные режимы, иначе постусловие превращается в большую и сложную формулу, трудную для анализа и понимания, что противоречит основной цели создания формальных спецификаций. Различные режимы работы операции описываются в виде импликаций с несовместными посылками (постусловие при этом выглядит как формула
\begin{lstlisting}
(X1 => Y1) /\
(X2 => Y2) /\ ...
(Xn => Yn)
\end{lstlisting}

или в виде разных выражений для возвращаемого результата при разных исходных условиях, т.е. результат постусловия вычисляется в разных ветвях некоторого условного оператора или оператора выбора по-разному. Поэтому эти разные режимы называют \emph{ветвями функциональности} операции.

%В двух словах, этот подход заключается в систематическом выделении фактов вида <<в 'такой-то' ситуации если выполнить при помощи системы 'такую-то' операцию, то пользователь получит в качестве результата 'то-то', а система перейдет в 'такое-то' состояние>>. На языке логики один такой факт выражается при помощи импликации $$\forall x~ ( ~p(x)~ \Rightarrow ~q(f(x)) ~)$$ а набор фактов --- конъюнкцией таких импликаций.
Например, при выполнении операции перехода по ссылке в одном из табов веб-браузера открывается новый таб или открывается новое окно с одним табом, или не открывается ни одного окна, ни одного таба (операция перехода по ссылке выполнилась --- и мы видим \emph{эффект этой операции}: открытие таба или открытие окна, или неоткрытие таба и неоткрытие новых окон, эффект операции в формуле выше обозначен как $q$). В этой модели нас будут интересовать только работа с табами при выполнении различных операций.

Под <<ситуацией>> будем понимать совокупность значений входных параметров, некие условия, при которых эффект операции обладает заданной спецификой (ситуация обозначена в формуле выше как $p$). Например, в ситуации, когда достигнут максимальный предел одновременно показываемых табов, при переходе по ссылке всегда открывается одно новое окно с одним табом. В этом \emph{функциональном требовании} операцией является <<переход по ссылке>>, ситуацией --- <<достигнут предел максимально показываемых табов и потребовано открытие нового таба>>, эффектом операции является <<открыто новое окно с одним новым табом>> (по-хорошему, этот эффект требует дополнения).

Еще несколько примеров. <<При выполнении операции закрытия таба все остальные табы остаются без изменений>> --- ситуация <<таб открыт>>, операция <<закрытие таба>>, эффект <<все табы, кроме закрываемого, не изменились>> (не изменилось их содержимое, заголовок и т.п., в зависимости от того, какие из характеристик таба входят в формальную модель). Заметьте, этот почти очевидный факт неполный. Он позволяет при закрытии таба изменить порядок табов. Тем самым, формальная модель системы с требованием <<при выполнении операции закрытия таба все остальные табы остаются без изменений>> содержит логику выполнения операции по закрытию таба с сохранением порядка и без сохранения порядка. Этот важный вывод о поведении системы получен чисто путем анализа формальной модели. Например, из этого следует, что нельзя утверждать, что если один таб создан позже другого, то всегда будет сохранен их относительный порядок один после другого. Это замечание может оказаться важным при проектировании других операций с табами, которые будут предполагать сохранение относительного расположения табов.

Возникает вопрос, какие факты нужно выделять, сколько фактов нужно выделять (когда фактов достаточно). %Если к выделению фактов подойти <<с особым рвением>>, то на каждое состояние системы и значения аргументов операций надо выписать отдельный факт: <<если система находится в 'таком-то' состоянии и аргументы равны 'тому-то', то при выполнении операции произойдет 'то-то'>> (например, если открыт один таб, то при выполнении операции закрытия табов в окне не останется ни одного таба - раз; если открыто два таба и закрывается первый таб, то при выполнении операции закрытия табов в окне остается бывший второй таб - два; если открыто два таба и закрывается второй таб, то при выполнении операции закрытия табов в окне остается бывший первый таб - три; уже получено три факта и это не предел!). Понятно, что так мельчить ситуации не имеет смысла как минимум, если эффект операции в этих ситуациях обладает некоторой общностью. Например, для операции закрытия таба может быть важно, в том же окне находится закрываемый таб, как и интересующие нас таб, или в другом (в первом случае, изменяется набор табов в окне, во втором случае не изменяется). Как минимум, следует выделить все ситуации для операции, в которых поведение системы обладает спецификой (чем-то важным отличается от поведения системы при выполнении операции в других ситуациях)\footnote{под поведением системы при выполнении операции понимается эффект операции}.%
Поскольку ситуации выражены на формальном языке, можно точно определить, покрывают ли эти ситуации все возможные ситуации, в которых будет выполняться операция. Например, если выделена только ситуация закрытия таба для своего окна, то <<для полноты картины>> нужна ситуация закрытия таба для окна без этого таба (если такие окна обладают дополнительной спецификой, влияющей на эффект закрытия таба, то требуется выделение для них дополнительных ситуаций). Полное выделение ситуаций --- первый залог того, что поведение системы в спецификации описано полно.

Следующий важный момент --- это слежение за замкнутостью модели. Речь идет вот, о чем. В правильной спецификации не может быть такого, что в результате выполнения операции в некоторой ситуации система приходит в такое состояние, про которое неизвестно, как себя будут вести операции, выполняющиеся из полученного состояния. Грубо говоря, есть строго определенное множество допустимых состояний системы, или \emph{инвариант} состояния системы, за которые операции не имеют права выводить систему. Например, инвариантами могут быть следующие факты: <<количество табов в окне не должно превысить максимально допустимое>>, <<в каждом окне должен быть как минимум один таб>>. Однако при проектировании операций придерживаются более гибкого подхода и допускается пересматривание инварианта, но в этом случае приходится перепроверять уже спроектированные операции для выявления того, во всех ли ситуациях описано их поведение и не требуется ли дополнительно определить поведение системы при выполнении операции из новых состояний, вошедших теперь в инвариант.

В некоторых ситуациях операция не может быть выполнена (например, нельзя закрыть единственный таб в окне --- это приведет к нарушению инварианта (в окне не останется ни одного таба). Знание о том, когда операция невозможна, так же важно, как и знание эффекта операции там, где операция возможна.

Подводя итог, можно предложить следующий подход к формализации поведения системы.

\begin{enumerate}
    \item сформулировать уровень абстракции (например, ограничиваемся рассмотрением логики работы с табами в рамках одного окна браузера);
    \item выделить множество операций и составить их сигнатуры (например, открытие нового таба, переход по ссылке, закрытие таба);
    \item сформулировать наиболее общий инвариант на состояние системы (под <<системой>> в данном случае понимается окно браузера с табами; например, в каждом окне должен быть как минимум 1 таб);
    \item далее действовать итеративно до получения полного замкнутого описания поведения системы при выполнении всех операций во всех ситуациях:
        \begin{itemize}
          \item выделить набор ситуаций на очередную операцию и описать эффект операции в этих ситуациях (как минимум, выделить ситуации, в которых операция невозможна);
          \item проверить, что эффект всех операций согласуется с инвариантом;
          \item при необходимости уточнить (усилить) инвариант или расширить (ослабить) инвариант --- при этом снова проверить соответствие эффекта операций во всех ситуациях.

%              все функции вызываются в согласии с предусловием
        \end{itemize}
\end{enumerate}

%% следить за тем, чтобы каждая формальная фраза могла быть неформально интерпретирована: общение между людьми ведь осуществляется неформальными фразами

В результате применения этого подхода к примеру с табами может получиться, например, следующая заготовка для функциональных требований:

{\sf
\textbf{Понятия}: Окно, Таб, Адрес

\textbf{Инварианты}:
\begin{enumerate}
  \item Окно есть совокупность табов;
  \item Табы в окне упорядочены;
  \item Все табы считаются различными;
  \item Табы содержатся в окнах, в табах окон нет;
  \item Каждому табу соответствует не более одного окна;
  \item В окне не может быть открыто табов больше некоторого максимума;
  \item Каждому табу соответствует некоторый один адрес или не соответствует никакого адреса.
\end{enumerate}
}

NB: Представьте, что браузер реализовали так, что какое-нибудь из этих \emph{свойств корректности} не выполнено. Можно ли считать такой браузер \emph{правильным} ?

При описании операций будет упомянуто требование \emph{тотальности}. Операция \emph{тотальная}, если ни при каких своих входных данных (т.е. ни при каких значениях, входящих в типы входных данных) она не может зациклиться или привести к аварийному останову системы. Иначе, операция называется \emph{частичная}. Требование тотальности на RSL можно указать. Для этого в сигнатуре соответствующей функции надо указать стрелку без тильды ($\rightarrow$).


{\sf
\textbf{Операция <<Открытие нового таба>>}

\begin{tabular}{|p{0.3\textwidth}|p{0.6\textwidth}|}
  \hline
  сигнатура & open: Окно $\NonDetermFn$ Окно $\times$ Таб \\ \hline
  тотальность & не требуется \\ \hline
  ситуации, когда операция невозможна & В Окне достигнут максимум одновременно открытых табов \\ \hline
  эффект операции в разных ситуациях & появляется один таб, в этом табе нет адреса, \underline{место этого таба пока не решено}, все остальные табы и их порядок остаются без изменений \\ \hline
\end{tabular}

\textbf{Операция <<Переход по ссылке>>}

\begin{tabular}{|p{0.3\textwidth}|p{0.6\textwidth}|}
  \hline
  сигнатура & go: Окно $\times$ Адрес $\times$ Таб $\NonDetermFn$ Окно \\ \hline
  тотальность & не требуется \\ \hline
  ситуации, когда операция невозможна & Таб не входит в Окно \\ \hline
  эффект операции в разных ситуациях & \begin{itemize}\item В ситуации, когда достигнут максимум одновременно открытых табов, заменяется адрес в Табе на Адрес, остальные табы и их порядок не меняются; \item В остальных ситуациях открывается новый таб и ему прописывается Адрес\end{itemize} \\ \hline
\end{tabular}

\textbf{Операция <<Закрытие существующего таба>>}

\begin{tabular}{|p{0.3\textwidth}|p{0.6\textwidth}|}
  \hline
  сигнатура & close: Окно $\times$ Таб $\NonDetermFn$ Окно \\ \hline
  тотальность & не требуется \\ \hline
  ситуации, когда операция невозможна & Таб не входит в Окно \\ \hline
  эффект операции в разных ситуациях & \begin{itemize}\item В ситуации, когда это единственный открытый таб, табу не соответствует никакой адрес;\item В остальных ситуациях Таб отсутствует, все остальные табы и их порядок сохраняются \end{itemize} \\ \hline
\end{tabular}
}

Выбрав подходящую модель состояния (на языке множеств, списков и отображений RSL), можно сформулировать инварианты состояния и программные контракты всех операций над системой.

\section{Программные контракты общего вида в RSL. Превыражения}

%Программный контракт операции --- это пара \emph{предусловие} операции и \emph{постусловие} операции. Предусловие --- это предикат на значениях входных данных операции (аргументы, состояние среды перед выполнением операции, внутреннее состояние модели перед выполнением операции). Постусловие --- это предикат на значениях входных и выходных данных операции (выходные данные --- это результат операции, состояние среды после выполнения операции, внутреннее состояние модели после выполнения операции). Смысл термина <<программный контракт>> раскрывается его названием: если операция вызвана с соблюдением предусловия, она должна проработать так, чтобы в результате соблюсти постусловие. Например, если операция взятия верхушки стека вызывается при стеке из одного элемента (это предусловие), операция вернет значение единственного хранящегося там элемента (это постусловие). 

%Согласно определению ничего не мешает иметь несколько пар <<предусловие - постусловие>> (если предусловия попарно не пересекаются). Тогда бы как только удовлетворен какое-нибудь предусловие, должно быть выполнено соответствующее ему постусловие (в этом есть своё удобство, если каждой парой описать отдельную <<ветвь функциональности>> операции, т.е. ситуацию, где поведение операции особенное). Однако так не делают и требуют указывать лишь одну пару <<предусловие - постусловие>>. В этой паре должно быть записано предусловие, объединяющее все ситуации, и постусловие, формулирующее требования к операции в каждой из ситуаций. Например, таким предусловием для операции взятия вершины стека является непустота стека.

Программные контракты общего вида --- это пара <<чистых>> логических выражений RSL (поствыражение и \emph{превыражение}), оформленных в виде имплицитного описания функции (<<чистое>> --- значит завершающееся детерминированное без побочных эффектов). Например:
\begin{lstlisting}
type Element, Stack = Element-list
value
   top : Stack -~-> Element
   top(s) as e
   post e = s(1)
   pre s ~= <..>
\end{lstlisting}

\emph{Превыражение} --- это <<чистое>> логическое выражение на тех входных данных, на которых имеет смысл стоящее перед ним определение функции или утверждение (об утверждениях будет разговор чуть позже). Например, в последнем примере функция top при непустом стеке должна быть такой, как сказано в поствыражении, а при пустом стеке \textbf{может быть какой угодно}. Превыражение ограничивает значения \emph{свободных переменных}, на которых формулируется утверждение и определение, в которое они входят. Для имплицитных описаний функций свободными переменными являются все входные данные (в последнем примере это s). Тем самым, написав превыражение, мы сказали, что данное имплицитное описание надо рассматривать не при всех s типа Stack (т.е. не для всех списков из Element), а только для непустых списков. Про пустые списки это описание ничего не говорит. 
%%%TODO а можно ли отдельно сказать про поведение функции top при пустом списке ? например, написав аксиому ...

Спецификация, в которой не сказано про поведение ряда операций при некоторых значениях входных данных, называется \emph{недоспецификацией}.

Однако пока неясно, можно ли при помощи превыражений и поствыражений выразить на RSL то, что удовлетворяет определениям постусловий и предусловий. С поствыражением вопросов никаких нет --- оно вполне может выполнять роль постусловия. Вопрос только с превыражением: может ли средство ограничения области, в которой делается данное утверждение, быть условием на среду, при выполнении которого гарантируется выполнение постусловия. На самом деле, поскольку можно написать только одно имплицитное/эксплицитное описание для операции, то и превыражение может быть сопоставлено только одно. Поэтому превыражение у имплицитного/эксплицитного описания может выполнять роль предусловия (в общем случае превыражение не выполняет роль предусловия).

Для рассматривавшейся ранее модели стека с операцией top:
\begin{lstlisting}
type Element, Stack = Element-list
value top : Stack -~-> Element
      top(s) is s(1)
      pre s ~= <..>
\end{lstlisting}
при предусловии <<стек непустой>> операция гарантирует возврат значения s(1), значит при совершении операции взятия вершины стека при пустом стеке может произойти всё, что угодно (операция может завершиться с возвратом какого-нибудь значения, зациклиться, аварийно остановиться). Но написав данное превыражение у определения, мы утверждаем, что при пустом стеке из текста эксплицитного описания нельзя сделать вывод о том, что произойдет при совершении операции взятия вершины стека. Этот пример ещё раз подчёркивает, что превыражение --- не является средством выражения предусловия в том же его понимании.

Напомним, что функция удовлетворяет \emph{требованию тотальности}, если она детерминированно завершается на каждом значении входных данных (на каждом значении из типов входных данных) и результат также соответствует типам выходных значений. Здесь стоит отметить, что если описание функции содержит превыражение и требование тотальности, то требование тотальности должно быть выполнено не только в области выполнимости превыражения, а даже в более широкой области (области значений типов входных данных). Например, в следующем описании:
\begin{lstlisting}
type Element, Stack = Element-list
value top : Stack -> Element
      top(s) is s(1)
      pre s ~= <..>
\end{lstlisting}
сказано, что при непустом стеке функция должна возвращать голову списка, а при пустом стеке функция должна возвращать некое значение в типе Element, но, какое именно, в спецификации не сказано.

В заключение хочется отметить, что контрактная спецификация операции (т.е. сформулированный набор её свойств) зависит от того, какое выбрано модельное состояние. Один вид модельного состояния позволяет сформулировать более конкретно и саму ситуацию, и эффект операции в ней, а другой, например, позволяет задать только допустимые эффекты операции.

%Советы из статьи Hints to Specifiers:
%1) думать не конкретными сценариями работы с системой, а в виде общих свойств
%2) абстрагироваться от вычислений (думать об отображении, осуществляемом операциями)
%3) думать не конкретно об этой модели, а сразу о классе моделей (т.е. строить "теорию" вместо построения "модели")
%4) действовать постепенно (сначала думать о предусловиях, затем о постусловиях, затем об ошибочных ситуациях)
%5) использовать недетерминизм (как абстракция от условий выбора разных альтернатив)
%6) использовать минимум операций для выражения свойств, остальные операции выразить через этот минимум
%7) использовать бесконечные сущности (бесконечные последовательности, бесконечные множества, вещественные числа бесконечной точности) 

%\section*{Задачи}
%TODO

\section{Финитные программные контракты}

Пост- и превыражения общего вида не всегда удобны для проверки, поскольку не любое логическое выражение в RSL можно вычислить. Например, такое выражение:
\begin{lstlisting}
 all x : Int :- exists y : Int :- x + y = 0
\end{lstlisting}
предполагало бы просмотр всех целых чисел (в качестве х) и для каждого х ещё один просмотр всех целых чисел (в поиске нужного y). Как легко заметить, оба эти просмотра не осуществимы за конечное время (ввиду бесконечности типа \textbf{Int}). Хотя понятно, что при вычислении логических выражений без кванторов таких проблем нет. Нет их и в тех случаях, если кванторы ограничены. \emph{Ограниченным квантором} будем называть следующие конструкции при конечном множестве ts:
\begin{lstlisting}
 all t : T :- t isin ts => ...
 exists t : T :- t isin ts /\ ... 
\end{lstlisting}
Такие кванторы могут быть легко превращены в заведома завершающийся обход множества. Аналогичная ситуация происходит при составлении множества:
\begin{lstlisting}
{ f(t) | t : T :- ... }
\end{lstlisting}
Назовем \emph{ограниченным конструктором множества} следующее выражение при конечном множестве ts:
\begin{lstlisting}
{ f(t) | t : T :- t isin ts /\ .... }
\end{lstlisting}
В этом случае можно вычислить значение такого множества, фильтруя элементы множества ts.

По аналогичной причине надо ограничить использование рекурсии в логических выражениях, поскольку вызов рекурсивной функции может привести к зацикливанию. К зацикливанию может привести и использование операторов цикла в поствыражениях.

Кроме того, использование функций, для которых нет эксплицитного описания, также невозможно в поствыражениях, предназначенных для вычисления. Это достаточно очевидно просто потому, что для вычисления выражения необходимо уметь вычислять значение всех входящих в это выражение функций, а если для такой функции нет эксплицитного описания, то вычислить ее зачастую нельзя.

Суммируя вышесказанное, назовем логическое выражение \emph{финитным}, если для него выполнены все следующие свойства:
\begin{enumerate}
\item все кванторы и конструкторы множеств, списков и отображений ограниченные;
\item нет рекурсии и операторов циклов;
\item нет вызовов функций без эксплицитного описания;
\item нет бесконечных сущностей (целых чисел бесконечного значения, вещественных чисел бесконечной точности, бесконечных типов-множеств, типов-списков, типов-отображений.
\end{enumerate}
Назовем \emph{финитными программными контрактами} такие программные контракты RSL, в которых поствыражение и превыражение являются финитными.

%\section*{Задачи}
%TODO

\section{Инварианты состояния}

Инвариант состояния --- это <<чистое>> логическое выражение. Это выражение выделяет среди всех состояний, допустимых его сигнатурой, некоторое подмножество. Это подмножество должно означать согласованные, допустимые, состояния. Например:
\begin{lstlisting}
type SortedList = Nat-list
axiom all s : SortedList :- sorted(s)
value
    sorted : Nat-list -> Bool
    sorted(s) is ( all i : Nat :- {i, i+1} <<= inds s => s(i) <= s(i+1) )  
\end{lstlisting}

т.е. после ключевого слова \textbf{axiom} идет квантор всеобщности с переменной типа модельного состояния, подкванторным выражением является инвариантное свойство.

\section*{Задачи}

\zhead{Описать функциональность операций}

В задачах этого типа требуется составить описание подобное тому, какое было составлено для <<Окон с Табами>>. Если данных в задаче недостаточно, требуется определить те ситуации, в которых поведение системы не описано, и доопределить поведение в таких ситуациях адекватным образом. В большинстве задач требуется выделить операции пользователя, которые выполняются посредством системы. У системы практически всегда есть внутреннее состояние. Если у сеанса работы с системой есть границы, то \textbf{правильная} система не должна позволять работать вне этих границ (до того, как начат сеанс, и после того, как становится известно, что сеанс закончен), например, играть в игру можно только до тех пор, пока игра не будет закончена. Не забыть про операции инициализации системы (например, когда начинается игра).

% декабрь-2009

\z <<Неазартное 'Двадцать одно'>>. Задача системы --- визуализировать поле игры в <<21>> (это карточная игра) и модифицировать его в ответ на команды игрока (т.е. в этой задаче не надо думать о всей программной системе для игры в Двадцать одно, надо думать только о том, по каким правилам должно <<работать>> содержимое поля игры). В колоде 36 карт разных мастей, каждая карта имеет свою стоимость. Играют двое: банкир и его соперник. Сначала соперник берет из колоды карт себе карты, затем банкир берет из колоды себе карты. Если сумма набранных баллов по картам у соперника равна 21, он выиграл; больше 21 - проиграл; иначе если у банкира 21, он выиграл; если больше 21 - проиграл; в противном случае выигрывает тот, кто набрал большую сумму баллов.

\z <<Шашки>>. Задача системы --- визуализировать поле игры в шашки и модифицировать это поле в ответ на команды игрока (т.е. в этой задаче не надо думать о всей программной системе для игры в шашки, надо думать только о том, по каким правилам надо работать с содержимым поля игры). Поле 8 на 8. У каждого игрока 12 шашек. Отличия от стандартных шашек: 1) бить назад нельзя, 2) бить несколько шашек нельзя, 3) дамок нет.


\z <<Домино>>. Задача системы --- визуализировать поле игры в домино и модифицировать это поле в ответ на команды игрока (т.е. в этой задаче не надо думать о всей программной системе для игры в домино, надо думать только о том, по каким правилам надо работать с содержимым поля игры). Играют двое. Вначале каждый игрок произвольным образом получает половину всех доминошек. Ход игрока заключается в выборе доминошки из своей кучи и вставки его линию с подходящего конца. Если игроку нечем походить, он проигрывает.

\z <<Пятнашки>>. Задача системы --- визуализировать поле игры в пятнашки и модифицировать это поле в ответ на команды игрока (т.е. в этой задаче не надо думать о всей программной системе для игры в домино, надо думать только о том, по каким правилам надо работать с содержимым поля игры). Поле 4 на 4 клетки. Все клетки, кроме одной, содержат фишку. Ход игрока состоит в том, что нужно передвинуть одну из фишек, соседствующих с пустой клеткой на пустое место. Цель игры --- выстроить фишки в соответствии с их номерами.

% январь-2010

% октябрь-2010

% декабрь-2010

% январь-2011
%TODO


%\zhead{Формализация требований согласно моделе-ориентированному подходу}

\z Написать спецификацию функции библиотеки POSIX \texttt{int fork()}. Эта функция позволяет создать дочерний процесс. Если дочерний процесс создан успешно, возвращается его идентификатор. В противном случае функция возвращает -1.

\textbf{Решение:}
\begin{lstlisting}
type Processes = Nat-set
value fork: Processes -~-> Processes >< Int
   fork(ps) as (ps2, pid)
   post pid = -1 /\ ps2 = ps
   	\/ pid >= 0 /\ pid ~isin ps /\ ps2 = ps union {pid}
\end{lstlisting}

Обратите внимание:
\begin{enumerate}
  \item поскольку в требованиях говорится только об идентификаторах, то только эта часть отражается в модели типа Processes. Для этой модели выбрано множество, т.к. все идентификаторы должны быть разными;
  \item эту функцию нельзя определить в эксплицитном виде с использованием выбранной модели состояния (типа Processes), т.к. нельзя сразу зафиксировать алгоритм генерации идентификаторов дочерних процессов (надо оставить свободу выбора этого алгоритма);
  \item в случае неуспешного создания процесса таблица процессов не меняется (явно это в требованиях не описано, но такое свойство имеет место);
  \item поскольку ничего не известно о детерминированности алгоритма генерации идентификаторов дочерних процессов, то использовано нетотальное определение.
\end{enumerate}

\z Написать спецификацию функции библиотеки POSIX \texttt{int fork()}. Эта функция позволяет создать дочерний процесс. Если дочерний процесс создан успешно, возвращается его идентификатор. В противном случае функция возвращает -1. После создания сегменты кода, данных и стека обоих процессов идентичны. Совпадают и счетчики инструкции. Необработанные сигналы родительского процесса в дочерний не наследуются. Считать, что для получения идентификатора текущего процесса есть функция \texttt{int getpid()}.

\textbf{Решение:}
\begin{lstlisting}
type Segment, Signal
type Process ::
		code : Segment,
		data : Segment,
		stack : Segment,
		instr_pntr : Nat,
		signals : Signal-list

type Processes = Nat -m-> Process

value getpid: Processes -~-> Int

value fork: Processes -~-> Processes >< Int
   fork(ps) as (ps2, pid)
   post pid = -1 /\ ps2 = ps
   	\/ pid >= 0 /\ pid ~isin dom ps /\ ps2 \ {pid} = ps /\
	let parent_id = getpid(ps), child = ps2(pid),
	     parent = ps(parent_id) in
   	       code(child) = code(parent) /\
   	       data(child) = data(parent) /\
   	       stack(child) = stack(parent) /\
   	       instr_pntr(child) = instr_pntr(parent) /\
   	       signals(child) = <..>
   	   end
\end{lstlisting}

Обратите внимание:
\begin{enumerate}
  \item по сравнению с предыдущей задачей модель типа Processes полностью изменилась (хотя требования лишь добавлялись), этот момент показывает важную особенность моделе-ориентированных спецификаций в отличие от алгебраических: модели типов могут меняться существенным образом при добавлении новых требований;
  \item на использование явного \textbf{let} для введения <<читабельных>> имен выражениям и повышения <<читабельности>> всего пост-выражения.
\end{enumerate}

\z Написать спецификацию функции библиотеки POSIX \texttt{int getpid()}. Эта функция позволяет получить идентификатор процесса, вызвавшего эта функцию.

\textbf{Решение:}
\begin{lstlisting}
type Processes = Nat-set
value getpid: Processes -~-> Int >< Processes
   getpid(ps) as (pid, ps2)
   post pid >= 0 /\ pid isin ps /\ ps2 = ps
\end{lstlisting}

Обратите внимание, что
\begin{enumerate}
  \item данная модель не позволяет дать алгоритм вычисления функции getpid (поэтому используется неявная спецификация), но позволяет тем не менее задать те свойства, которые перечислены в постановке задачи;
  \item хоть модель и довольно простая, но она наглядная и позволяет ее читать и делать выводы относительно функции getpid даже тому, кто не знает POSIX;
  \item пост-выражение можно эквивалентным образом сократить до такого: pid $\Isin$ ps $\wedge$ ps = ps2, поскольку в ps входят только натуральные числа.
\end{enumerate}

% \z exec
% остальные функции ........

%\section{Согласованность модельных спецификаций}

%..........TODO

% \zhead задачи на анализ спецификаций (а то зачем же они нужны, если, кроме как написать, с ними ничего не сделать!)

%\subsection*{Задачи}
%.........TODO



%\section{Уточнение требований при помощи алгебр}
%
%\section{Согласованность алгебраических спецификаций}
%
%\section{Алгебраические спецификации и конечные автоматы}

\chapter{Инструмент Dafny}

Инструмент Dafny\footnote{название инструмента является смесью букв слов dynamic frames} позволяет задать и верифицировать функциональность <<классов>>. <<Объект>> <<класса>> содержит состояние, согласованность которых должны поддерживать \emph{методы} класса. Методам можно указать предусловие (requires) и постусловие (ensures). Если написано тело метода (некая реализация программного контракта), Dafny пытается автоматически доказать выполнение контракта реализацией методов. Если это не удается сделать, Dafny выдает сообщение об ошибке. Реализация метода осуществляется на языке инструмента Dafny императивного стиля. Dafny пытается доказать, что реализация завершается на данных, удовлетворяющих предусловию. Для этого он требует указания инварианта цикла (invariant) и условия завершимости (decreases). Условия завершимости нужно указывать и для рекурсивных функций.

Более подробно об инструменте можно прочитать в статьях на сайте http://research.microsoft.com/en-us/projects/dafny/.

Вам предлагается выполнить ряд упражнений не столько с целью освоения инструмента Dafny, сколько для выработки навыка написания программных контрактов и других аннотаций для верификации кода. Если Dafny успешно всё доказал, значит спецификация составлена правильно. Если что-то Dafny не смог доказать, значит либо не полностью описаны программные контракты/инварианты, либо они слишком сложные для автоматического доказательства (для подсказок инструменту Dafny надо писать т.н. ghost methodы). Задачи подобраны таким образом, что возможно их решить, не прибегая к ghost methodам. Кроме того, предлагаемые здесь задачи не предполагают спецификации операций с памятью.

Если не удается понять, почему Dafny не может доказать то или иное свойство, попробуйте подобавлять assert в разные точки реализации с предполагаемыми тождественно верными выражениями. Если Dafny сообщит о невыполнении одного из assert, то надо проанализировать причину этого и в результате понять, где ошибка.

Dafny можно установить в виде дополнения среды разработки Visual Studio 2010, можно запускать в виде утилиты командной строки (но перед этим надо не забыть установить решатель Z3 версии 2.15), но проще всего пользоваться инструментом Dafny из браузера. Для этого надо зайти на сайт http://rise4fun.com/dafny/, написать текст методов и аннотаций и нажать кнопку ask dafny. Если Dafny сообщит о ряде проблем, можно нажать на строчку с проблемой и место проблемы будет подсвечено.

\section*{Задачи}

\zhead{Восстановить инвариант цикла}

\z (http://rise4fun.com/Dafny/t3F) Автор хотел реализовать умножение двух чисел. Напишите инвариант цикла и найдите (и исправьте) ошибку в реализации.
\begin{verbatim}
method fi(x: int, y : int) returns (z: int)
   requires x >= 0 && y >= 0;
   ensures  z == x * y;
{
   var i := 0;
   while (i < y)
     invariant ...........;
   {
       i := i + 1;
       z := z + x;
   }
}
\end{verbatim}

\z (http://rise4fun.com/Dafny/yqQ) Автор хотел реализовать умножение двух чисел. Напишите инвариант цикла и найдите (и исправьте) ошибку в реализации.
\begin{verbatim}
method fi(x: int, y : int) returns (z: int)
   requires x >= 0 && y >= 0;
   ensures  z == x * y;
{
   var i := y;
   while (i > 0)
     invariant ...........;
   {
       i := i - 1;
       z := z + x;
   }
}
\end{verbatim}

\z (http://rise4fun.com/Dafny/4Xe)
\begin{verbatim}
method sqrt(x : nat) returns (s : int)
   ensures s*s <= x < (s+1)*(s+1);
{
   s := 0;
   while ((s+1)*(s+1) <= x)
       invariant ........;
   {
     s := s + 1;
   }
}
\end{verbatim}

\z (http://rise4fun.com/Dafny/poC)
\begin{verbatim}
method search(a : array<int>, key : int) returns (b: bool)
   requires ....;
   ensures b <==> exists i :: 0 <= i < a.Length  && a[i] == key;
{
     var n := a.Length - 1;
     if (n < 0)
     {
         return false;
     }

     while (a[n] != key)
       decreases ....;
       invariant ....;
     {
         n := n - 1;
         if (n < 0)
         {
            break;
         }
     }
     return 0 <= n;
}
\end{verbatim}

\z (http://rise4fun.com/Dafny/Qch) Напишите спецификацию и реализацию метода вычисления кубов натуральных чисел, помещающего в i-й элемент массива i*i*i. Добейтесь того, чтобы Dafny успешно верифицировал реализацию. Затем модифицируйте реализацию таким образом, чтобы она не использовала умножения, только сложения.

\begin{verbatim}
method Cubes(a: array<int>)
  modifies a;
{
}
\end{verbatim}

\z (http://rise4fun.com/Dafny/6xO) Напишите спецификацию и \textbf{рекурсивную} реализацию метода вычисления кубов натуральных чисел, помещающего в i-й элемент массива i*i*i. Реализация не должна использовать умножения, только сложения.
\begin{verbatim}
method Cubes(a: array<int>)
  modifies a;
{
}
\end{verbatim}

\z (http://rise4fun.com/Dafny/6bq) Напишите спецификацию, при которой Dafny докажет правильность реализации. Нужно написать постусловие и decreases, предусловие писать не нужно. Имя метода подскажет его смысл.
method NinetyOne(n: int) returns (r: int)
{
  if (100 < n) {
    r := n - 10;
  } else {
    r := NinetyOne(n + 11);
    r := NinetyOne(r);
  }
}

\z (http://rise4fun.com/Dafny/WvG) Метод в этой задаче возвращает истину тогда и только тогда, когда последовательности f и g имеют общий элемент. Напишите и верифицируйте реализацию, временная сложность которой O(|f| + |g|), а не O(|f|*|g|).

\begin{verbatim}
method Coincidence(f: seq<int>, g: seq<int>) returns (r: bool)
  requires forall i, j :: 0 <= i <= j < |f| ==> f[i] <= f[j];
  requires forall i, j :: 0 <= i <= j < |g| ==> g[i] <= g[j];
  ensures r <==> exists m :: m in f && m in g;
{
}
\end{verbatim}



\chapter{Аналитическая верификация}

\section{Методы Флойда}

\section*{Задачи}

Во всех задачах $x_1, x_2, ...$ --- входные переменные, $y_1, y_2, ...$ --- промежуточные переменные, $z_1, z_2, ...$ --- выходные переменные. Если не сказано противное, входные переменные обладают целыми неотрицательными значениями.

Если в алгоритмах не указано условие у оператора цикла, значит это условие --- тождественная истина (т.е. цикл бесконечный).

\zhead{Доказать частичную корректность следующих числовых алгоритмов\footnote{Часть задач взяты из~\cite{Shen}, часть задач составлены Алексеем Хорошиловым}}

\z $pre(x_1, x_2)~is~true$, $post(x_1, x_2, z)~is~(z = x_1 \cdot x_2)$

\begin{codebox}
\Procname{$\proc{Multiply}(x_1,x_2)$}
\li $y_1 \gets 0$
\li $y_2 \gets 1$
\li \While $y_2 \leq x_2$
\li \Do $(y_1,~y_2) \gets (y_2 + x_1,~y_2 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1)~is~true$, $post(x_1, z)~is~(z = x_1 \cdot (x_1 + 1))$

\begin{codebox}
\Procname{$\proc{Arithmetic}(x_1)$}
\li $y_1 \gets 0$
\li $y_2 \gets 1$
\li \While $y_2 \leq x_1$
\li \Do $(y_1,~y_2) \gets (y_1 + 2y_2,~y_2 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1)~is~true$, $post(x_1, z)~is~(z = x_1 \cdot (x_1 + 1) \cdot (2x_1 + 1))$

\begin{codebox}
\Procname{$\proc{SumSquare}(x_1)$}
\li $y_1 \gets 0$
\li $y_2 \gets 1$
\li \While $y_2 \leq x_1$
\li \Do $(y_1,~y_2) \gets (y_1 + 6y_2\cdot y_2,~y_2 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~true$, $post(x_1, x_2, z)~is~(z = x_1^{x_2})$

\begin{codebox}
\Procname{$\proc{Power}(x_1,x_2)$}
\li $y_1 \gets 1$
\li $y_2 \gets 1$
\li \While $y_2 \leq x_2$
\li \Do $(y_1,~y_2) \gets (y_1 * x_1,~y_2 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~(x_2 > 0)$, $post(x_1, x_2, z)~is~(z = x_1^{x_2})$

\begin{codebox}
\Procname{$\proc{Power}(x_1,x_2)$}
\li $y_1 \gets x_1$
\li $y_2 \gets 1$
\li \While $y_2 < x_2$
\li \Do \If $2y_2 \leq x_2$
\li \Then $(y_1,~y_2) \gets (y_1 * y_1,~2y_2)$
\li \Else $(y_1,~y_2) \gets (y_1 * x_1,~y_2 + 1)$ \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~true$, $post(x_1, x_2, z)~is~(z = x_1^{x_2})$

\begin{codebox}
\Procname{$\proc{Power}(x_1,x_2)$}
\li $y_1 \gets 1$
\li $y_2 \gets 0$
\li \While $y_2 < x_2$
\li \Do \If $y_2 = 0$
\li \Then $(y_1,~y_2) \gets (x_1,~1)$
\li \Else \If $2y_2 \leq x_2$
\li \Then $(y_1,~y_2) \gets (y_1 * y_1,~2y_2)$
\li \Else $(y_1,~y_2) \gets (y_1 * x_1,~y_2 + 1)$ \End \End \End
\li $z \gets y_1$
\end{codebox}

% НОД
\z (<<GCD>> -- greatest common divisor) $pre(x_1, x_2)~is~(x_1 + x_2 > 0)$, $post(x_1, x_2, z)~is~(z = \gcd(x_1,x_2))$

\begin{codebox}
\Procname{$\proc{GCD}(x_1,x_2)$}
\li \If $x_1 > x_2$
\li \Then $y_1 \gets x_1$
\li \Else $y_1 \gets x_2$ \End
\li \While $x_1 \mod y_1 \neq 0 ~\vee~ x_2 \mod y_1 \neq 0$
\li \Do $y_1 \gets y_1 - 1$ \End
\li $z \gets y_1$
\end{codebox}

\z (<<GCD>> -- greatest common divisor) $pre(x_1, x_2)~is~(x_1 + x_2 > 0)$, $post(x_1, x_2, z)~is~(z = \gcd(x_1,x_2))$

\begin{codebox}
\Procname{$\proc{GCD}(x_1,x_2)$}
\li $y_1 \gets x_1$
\li $y_2 \gets x_2$
\li \While $y_1 > 0 ~\wedge~ y_2 > 0$
\li \Do \If $y_1 \geq y_2$
\li     \Then $y_1 \gets y_1 - y_2$
\li     \Else $y_2 \gets y_2 - y_1$ \End \End
\li \If $y_1 = 0$
\li \Then $z \gets y_2$
\li \Else $z \gets y_1$ \End
\end{codebox}

\z (<<LCM>> -- least common multiple) $pre(x_1, x_2)~is~(x_1 + x_2 > 0)$, $post(x_1, x_2, z)~is~(z = 2\cdot \mbox{lcm}(x_1,x_2))$

\begin{codebox}
\Procname{$\proc{2LCM}(x_1,~x_2)$}
\li $(y_1,~y_2,~y_3,~y_4) \gets (x_1,~x_2,~x_2,~x_1)$
\li \While $y_1 \neq 0 ~\wedge~ y_2 \neq 0$
\li \Do \If $y_1 \geq y_2$
\li     \Then $(y_1,~y_4) \gets (y_1 - y_2,~y_3 + y_4)$
\li     \Else $(y_2,~y_3) \gets (y_2 - y_1,~y_3 + y_4)$ \End \End
\li \If $y_1 = 0$
\li \Then $z \gets y_4$
\li \Else $z \gets y_3$ \End
\end{codebox}

\z $pre(x)~is~true$, $post(x, z)~is~(z = x^2)$

\begin{codebox}
\Procname{$\proc{Square}(x)$}
\li $(y_1,~y_2,~y_3) \gets (0,~0,~0)$
\li \While $y_1 < x$
\li \Do $(y_1,~y_2,~y_3) \gets (y_1 + 1,~y_2 + 2,~y_2 + y_3)$ \End
\li $z \gets y_1 + y_3$
\end{codebox}

\z $pre(x)~is~true$, $post(x, z)~is~(z^2 \leq x < (z+1)^2)$

\begin{codebox}
\Procname{$\proc{Sqrt}(x)$}
\li $(y_1,~y_2,~y_3) \gets (0,~0,~1)$
\li \While
\li \Do $y_2 \gets y_2 + y_3$
\li \If $y_2 > x$
\li \Then break
\li \Else $(y_1,~y_3) \gets (y_1 + 1,~y_3 + 2)$ \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~(x_1 > 0)~\wedge~(x_2 > 0)$, $post(x_1, x_2, z_1, z_2)~is~(0 \leq z_2 < x_2)~\wedge~(x_1 = z_1 \cdot x_2 + z_2)$

\begin{codebox}
\Procname{$\proc{Division}(x_1, x_2)$}
\li $(y_1,~y_2,~y_3) \gets (0,~0,~x_1)$
\li \While $y_3 \neq 0$
\li \Do $y_1 \gets if~(y_2 + 1 = x_2)~then~(y_1 + 1)~else~y_1$
\li     $y_2 \gets if~(y_2 + 1 = x_2)~then~0~else~(y_2 + 1)$
\li     $y_3 \gets y_3 - 1$ \End
\li $(z_1,~z_2) \gets (y_1,~y_2)$
\end{codebox}

\z $pre(x)~is~true$, $post(x, z)~is~(z = x^2)$

\begin{codebox}
\Procname{$\proc{Square}(x)$}
\li $(y_1,~y_2,~y_3) \gets (0,~1,~1-x)$
\li \While $y_3 < x$
\li \Do \If $odd(y_2)$
\li     \Then $y_1 \gets y_1 + y_2$ \End
\li     $(y_2,~y_3) \gets (y_2 + 1,~y_3 + 1)$ \End
\li $z \gets y_1$
\end{codebox}

$odd(x)$ истинно тогда и только тогда, когда $x$ нечетно.

\z $pre(x)~is~true$, $post(x, z)~is~(z^3 \leq x < (z+1)^3)$

\begin{codebox}
\Procname{$\proc{Cubert}(x)$}
\li $(y_1,~y_2,~y_3) \gets (0,~0,~1)$
\li \While
\li \Do $y_2 \gets y_2 + y_3$
\li     \If $y_2 > x$
\li     \Then break
\li     \Else $y_1 \gets y_1 + 1$
\li             $y_3 \gets y_3 + 6y_1$ \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x)~is~(x < 102)$, $post(x, z)~is~(z = 91)$

\begin{codebox}
\Procname{$\proc{Century}(x)$}
\li $(y_1,~y_2) \gets (x,~1)$
\li \While $y_1 < 101 ~\vee~ y_2 \neq 1$
\li \Do \If $y_1 > 100$
\li     \Then $(y_1,~y_2) \gets (y_1 - 10,~y_2 - 1)$
\li     \Else $(y_1,~y_2) \gets (y_1 + 11,~y_2 + 1)$ \End \End
\li $z \gets y_1 - 10$
\end{codebox}

\z $pre(x)~is~(x > 1)$, $post(x, z)~is~(z = x^3)$

\begin{codebox}
\Procname{$\proc{Qube}(x)$}
\li $(y_1,~y_2,~y_3) \gets (x,~1,~x)$
\li \While
\li \Do \If $y_2 < y_3$
\li     \Then $(y_1,~y_2) \gets (y_1 + x,~y_2 + 1)$
\li     \Else \If $y_3 = x$
\li         \Then $y_3 \gets y_1$
\li         \Else break \End \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x)~is~true$, $post(x, z)~is~(z = x^2)$

\begin{codebox}
\Procname{$\proc{Square}(x)$}
\li $(y_1,~y_2) \gets (x,~1)$
\li \While $y_2 < x$
\li \Do \If $2y_2 \leq x$
\li     \Then $(y_1,~y_2) \gets (2y_1,~2y_2)$
\li     \Else $(y_1,~y_2) \gets (y_1 + x,~y_2 + 1)$ \End \End
\li $z \gets y_1$
\end{codebox}

\z $pre(x_1, x_2)~is~true$, $post(x_1, x_2, z)~is~(z = {x_1}^{x_2})$ ($0^0~is~1$)

\begin{codebox}
\Procname{$\proc{Power}(x)$}
\li $(y_1,~y_2,~y_3) \gets (x_1,~x_2,~1)$
\li \While $y_2 \neq 0$
\li \Do \If $odd(y_2)$
\li     \Then $(y_2,~y_3) \gets (y_2 - 1,~y_1 \cdot y_3)$
\li     \Else $(y_1,~y_2) \gets (y_1 \cdot y_1,~y_2 / 2)$ \End \End
\li $z \gets y_3$
\end{codebox}

$odd(x)$ истинно тогда и только тогда, когда $x$ нечетно.



% дискретное логарифмирование


%\section{Инструмент PVS}
%...........TODO


%%%\chapter{Алгебраические спецификации}
%%%TBD
%%%\chapter{Поведенческие спецификации}
%%%TBD
%%%\chapter{Спецификации процессов}
%%%TBD
%%



%\chapter{Формальные спецификации в различных предметных областях}


%%\chapter{Специфицирование систем реального размера}
%%Спецификация для функции append в <<исполнимой>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value append: L >< L -> L
%%    append(x, y) is x ^ y
%%\end{lstlisting}
%%
%%Спецификация для функции append в <<логической>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value append: L >< L -> L
%%    append(x, y) as z
%%    post
%%        len z = len x + len y /\
%%        ( all i: Nat :- i isin inds x => z(i) = x(i)) /\
%%        ( all i: Nat :- i isin inds y => z(i+len x) = y(i))
%%\end{lstlisting}
%%
%%Спецификация для функции reverse в <<исполнимой>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value reverse: L -> L
%%    reverse(x) is
%%        local variable y : L :- y = <..> in
%%            for xi in x do
%%                y := <.xi.> ^ y
%%            end;
%%            y;
%%        end
%%\end{lstlisting}
%%
%%Спецификация для функции reverse в <<логической>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value reverse: L -> L
%%  reverse(x) as y
%%  post len x = len y /\
%%    ( all i: Nat :- i isin inds x => y(i) = x(len x + 1 - i))
%%\end{lstlisting}
%%
%%Спецификация для функции reverse в <<алгебраической>> манере:
%%\begin{lstlisting}
%%type E, L = E*
%%value reverse: L -> L
%%axiom
%%    reverse(<..>) is <..>,
%%    all x, y: L :- reverse(x^y) is reverse(y) ^ reverse(x)
%%\end{lstlisting}
%%
%%Что из этого короче? Что понятнее? Что лучше? (зависит от задачи)
%
%% задача - выбрать и правильно смоделировать самое главное в алгоритме:
%% gzip, протокол MESI, map/reduce, mp3, google chrome... (в зависимости от варианта задания--посмотреть,что интересует молодежь на Хабре) -- так, чтобы другой человек мог сам понять и получить это новое знание. В качестве примера, можно рассмотреть то, что я писал в диссертации - поймут студенты?
%% DOM:
%%http://www.w3.org/TR/DOM-Level-3-Core/core.html#ID-184E7107–???DOM Core 3
%%http://ru.wikipedia.org/wiki/Document_Object_Model-

\appendix
\include{rslprior}

\pagebreak
\addcontentsline{toc}{chapter}{Литература}
\bibliographystyle{gost780s}
\bibliography{rslbooks}

\end{document}
